M:MsgA, x:Id, s1, s2:M.(timed)state.
ma-x-tequiv(M;x;s1;s2)  ma-x-tequiv(M;x;shift-state(s1);shift-state(s2)) 

latex

Definitions	, , t  T, x:AB(x), x:A. B(x), #$n, r + s, f(a), x.A(x), <a, b>, M.ds(x), s = t, MsgA, Id, , A, P  Q, timedState(ds), ma-x-tequiv(M;x;s1;s2), shift-state(s), M.(timed)state, s ~ t, {T}, SQType(T)
Lemmas	not wf, ma-ds wf, Id wf, msga wf, qadd wf, int inc rationals, rationals wf